Nuprl Definition : sorted
0,22
postcript
pdf
sorted(
L
) ==
i
:
||
L
||,
j
:
i
.
L
[
j
]
L
[
i
]
latex
clarification:
sorted(
L
) ==
i
:{0..||
L
||
},
j
:{0..
i
}.
L
[
j
]
L
[
i
]
latex
Definitions
||
as
||
,
x
:
A
.
B
(
x
)
,
{
i
..
j
}
,
A
B
,
l
[
i
]
FDL editor aliases
sorted
origin
i:
||L||, j:i. L[j]
L[i]
i:{0..||L||
}, j:{0..i}. L[j]L[i] i:||L||, j:i. L[j]L[i]
i:{0..||L||}, j:{0..i}. L[j]L[i] x:A. B(x)}B